1 /-
2 Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Sébastien Gouëzel
5 -/
6
7 import topology.metric_space.basic analysis.specific_limits
src └─────────────────────────┘ └──────────────────────┘
8
9 /-!
10 # Baire theorem
11
12 In a complete metric space, a countable intersection of dense open subsets is dense.
13
14 The good concept underlying the theorem is that of a Gδ set, i.e., a countable intersection
15 of open sets. Then Baire theorem can also be formulated as the fact that a countable
16 intersection of dense Gδ sets is a dense Gδ set. We prove Baire theorem, giving several different
17 formulations that can be handy. We also prove the important consequence that, if the space is
18 covered by a countable union of closed sets, then the union of their interiors is dense.
19
20 The names of the theorems do not contain the string "Baire", but are instead built from the form of
21 the statement. "Baire" is however in the docstring of all the theorems, to facilitate grep searches.
22 -/
23
24 noncomputable theory
25 open_locale classical
26
27 open filter lattice encodable set
28
29 variables {α : Type*} {β : Type*} {γ : Type*}
30
31 section is_Gδ
32 variable [topological_space α]
id └───────────────┘
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
33
34 /-- A Gδ set is a countable intersection of open sets. -/
35 def is_Gδ (s : set α) : Prop :=
id └─┘ ┴
src └─┘
typ └─┘ ┴
36 ∃T : set (set α), (∀t ∈ T, is_open t) ∧ countable T ∧ s = (⋂₀ T)
id ┴ └─┘ └─┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ └┘ ┴
src ┴ └─┘ └─┘ ┴ ┴ └─────┘ ┴ └───────┘ ┴ ┴ └┘
typ ┴ └─┘ └─┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ └┘ ┴
doc └─────┘ └───────┘ └┘
37
38 /-- An open set is a Gδ set. -/
39 lemma is_open.is_Gδ {s : set α} (h : is_open s) : is_Gδ s :=
id └─┘ ┴ └─────┘ ┴ └───┘ ┴
src └─┘ └─────┘ └───┘
typ └─┘ ┴ └─────┘ ┴ └───┘ ┴
doc └─────┘ └───┘
40 ⟨{s}, by simp [h], countable_singleton _, (set.sInter_singleton _).symm⟩
id └─────────────────┘ └──────────────────┘
src └────┘ ┴ └─────────────────┘ └──────────────────┘
typ └────┘ ┴ └─────────────────┘ └──────────────────┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
41
42 lemma is_Gδ_bInter_of_open {ι : Type*} {I : set ι} (hI : countable I) {f : ι → set α}
43 (hf : ∀i ∈ I, is_open (f i)) : is_Gδ (⋂i∈I, f i) :=
44 ⟨f '' I, by rwa ball_image_iff, countable_image _ hI, by rw sInter_image⟩
src └──┘ └─┘
typ └──┘ └─┘
doc └──┘ └─┘
txt └──┘ └─┘
par └──┘ └─┘
pid ┴ ┴
45
46 lemma is_Gδ_Inter_of_open {ι : Type*} [encodable ι] {f : ι → set α}
47 (hf : ∀i, is_open (f i)) : is_Gδ (⋂i, f i) :=
id ┴ └───┘ ┴┴┴ ┴ ┴
src └───┘ ┴ ┴
typ ┴ └───┘ ┴┴┴ ┴ ┴
doc └───┘ ┴ ┴
48 ⟨range f, by rwa forall_range_iff, countable_range _, by rw sInter_range⟩
id └───┘ ┴ └──────────────┘ └─────────────┘ └──────────┘
src └───┘ └──┘└──────────────┘ └─────────────┘ └─┘└──────────┘
typ └───┘ ┴ └──┘└──────────────┘ └─────────────┘ └─┘└──────────┘
doc └───┘ └──┘ └─┘
txt └──┘ └─┘
par └──┘ └─┘
pid ┴ ┴
st └───────────────────┘ └──────────────┘
49
50 /-- A countable intersection of Gδ sets is a Gδ set. -/
51 lemma is_Gδ_sInter {S : set (set α)} (h : ∀s∈S, is_Gδ s) (hS : countable S) : is_Gδ (⋂₀ S) :=
id └─┘ └─┘ ┴ ┴ ┴ └───┘ ┴ └───────┘ ┴ └───┘ └┘ ┴
src └─┘ └─┘ └───┘ └───────┘ └───┘ └┘
typ └─┘ └─┘ ┴ ┴ ┴ └───┘ ┴ └───────┘ ┴ └───┘ └┘ ┴
doc └───┘ └───────┘ └───┘ └┘
52 begin
53 have : ∀s : set α, ∃T : set (set α), s ∈ S → ((∀t ∈ T, is_open t) ∧ countable T ∧ s = (⋂₀ T)),
id └─┘ └─┘ ┴ ┴ ┴ ┴ └─────┘ ┴ └───────┘ ┴ └┘
src └─────┘ └──┘ ┴ ┴ └──┘ ┴ └─┘┴ ┴┴┴ ┴ ┴ ┴ ┴ └──┘ ┴└─────┘┴ └┘┴┴└───────┘┴ ┴ ┴ ┴┴┴ └┘┴ └┘
typ └─────┘ └──┘ ┴ ┴ └──┘└─┘┴ └─┘┴┴┴┴┴ ┴┴┴┴┴ ┴ └──┘ ┴└─────┘┴ └┘┴┴└───────┘┴ ┴ ┴ ┴┴┴ └┘┴ └┘
doc └─────┘ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴└─────┘┴ └┘ ┴└───────┘┴ ┴ ┴ ┴ ┴ └┘┴ └┘
txt └─────┘ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
par └─────┘ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
pid └───┘└┘ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
st └─────────────────────────────────────────────────────────────────────┘└─
54 { assume s,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───┘└──────┘└─
55 by_cases hs : s ∈ S,
id ┴ ┴
src └───────┘ └─┘ ┴ ┴
typ └───────┘ └─┘┴┴ ┴┴
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ──────────────────────┘└─
56 { simp [hs], exact h s hs },
id └┘ ┴ ┴ └┘
src └────┘ ┴ └────┘ ┴ ┴ ┴
typ └────┘└┘┴ └────┘┴┴┴┴└┘┴
doc └────┘ ┴ └────┘ ┴ ┴ ┴
txt └────┘ ┴ └────┘ ┴ ┴ ┴
par └────┘ ┴ └────┘ ┴ ┴ ┴
pid ┴┴ ┴ ┴ ┴ ┴ ┴
st ─────┘└───────┘└─────────────┘└┘└
57 { simp [hs] }},
id └┘
src └────┘ └┘
typ └────┘└┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ───────────────┘└─┘└
58 choose T hT using this,
id └──┘
src └────────────────┘
typ └────────────────┘└──┘
doc └────────────────┘
txt └────────────────┘
par └────────────────┘
pid └┘└─┘└─────┘
st ───────────────────────┘└─
59 refine ⟨⋃s∈S, T s, λt ht, _, _, _⟩,
id ┴ ┴┴ ┴
src └─────┘ ┴└┘ ┴┴ ┴ └┘ └────────────┘
typ └─────┘ ┴└┘┴┴┴┴┴ └┘ └────────────┘
doc └─────┘ ┴└┘ ┴┴ ┴ └┘ └────────────┘
txt └─────┘ └┘ ┴ ┴ └┘ └────────────┘
par └─────┘ └┘ ┴ ┴ └┘ └────────────┘
pid ┴ └┘ ┴ ┴ └┘ └────────────┘
st ───────────────────────────────────┘└─
60 { simp only [exists_prop, set.mem_Union] at ht,
id └─────────┘ └───────────┘
src └─────────┘└─────────┘└┘└───────────┘└─────┘
typ └─────────┘└─────────┘└┘└───────────┘└─────┘
doc └─────────┘ └┘ └─────┘
txt └─────────┘ └┘ └─────┘
par └─────────┘ └┘ └─────┘
pid ┴└──┘└┘ └┘ ┴┴└───┘
st ───┘└──────────────────────────────────────────┘└─
61 rcases ht with ⟨s, hs, tTs⟩,
id └┘
src └─────┘ └────────────────┘
typ └─────┘└┘└────────────────┘
doc └─────┘ └────────────────┘
txt └─────┘ └────────────────┘
par └─────┘ └────────────────┘
pid ┴ └────────────────┘
st ──────────────────────────────┘└─
62 exact (hT s hs).1 t tTs },
id └┘ ┴ └┘ ┴ └─┘
src └────┘ ┴ ┴ └──┘ ┴ ┴
typ └────┘ └┘┴┴┴└┘└──┘┴┴└─┘┴
doc └────┘ ┴ ┴ └──┘ ┴ ┴
txt └────┘ ┴ ┴ └──┘ ┴ ┴
par └────┘ ┴ ┴ └──┘ ┴ ┴
pid ┴ ┴ ┴ └──┘ ┴ ┴
st ───────────────────────────┘└┘└
63 { exact countable_bUnion hS (λs hs, (hT s hs).2.1) },
id └──────────────┘ └┘ └┘
src └────┘└──────────────┘┴ ┴ └────┘ ┴ ┴ └─────┘
typ └────┘└──────────────┘┴└┘┴ └────┘ └┘┴ ┴ └─────┘
doc └────┘ ┴ ┴ └────┘ ┴ ┴ └─────┘
txt └────┘ ┴ ┴ └────┘ ┴ ┴ └─────┘
par └────┘ ┴ ┴ └────┘ ┴ ┴ └─────┘
pid ┴ ┴ ┴ └────┘ ┴ ┴ └────┘┴
st ───┘└───────────────────────────────────────────────┘└┘└
64 { exact (sInter_bUnion (λs hs, (hT s hs).2.2)).symm }
id └───────────┘ └┘
src └────┘ └───────────┘┴ └────┘ ┴ ┴ └───────────┘
typ └────┘ └───────────┘┴ └────┘ └┘┴ ┴ └───────────┘
doc └────┘ ┴ └────┘ ┴ ┴ └───────────┘
txt └────┘ ┴ └────┘ ┴ ┴ └───────────┘
par └────┘ ┴ └────┘ ┴ ┴ └───────────┘
pid ┴ ┴ └────┘ ┴ ┴ └─────────┘└┘
st ─────────────────────────────────────────────────────┘└─
65 end
st ──┘
66
67 /-- The union of two Gδ sets is a Gδ set. -/
68 lemma is_Gδ.union {s t : set α} (hs : is_Gδ s) (ht : is_Gδ t) : is_Gδ (s ∪ t) :=
id └─┘ ┴ └───┘ ┴ └───┘ ┴ └───┘ ┴ ┴ ┴
src └─┘ └───┘ └───┘ └───┘ ┴
typ └─┘ ┴ └───┘ ┴ └───┘ ┴ └───┘ ┴ ┴ ┴
doc └───┘ └───┘ └───┘
69 begin
st └─────
70 rcases hs with ⟨S, Sopen, Scount, sS⟩,
id └┘
src └─────┘ └──────────────────────────┘
typ └─────┘└┘└──────────────────────────┘
doc └─────┘ └──────────────────────────┘
txt └─────┘ └──────────────────────────┘
par └─────┘ └──────────────────────────┘
pid ┴ └──────────────────────────┘
st ──────────────────────────────────────┘└─
71 rcases ht with ⟨T, Topen, Tcount, tT⟩,
id └┘
src └─────┘ └──────────────────────────┘
typ └─────┘└┘└──────────────────────────┘
doc └─────┘ └──────────────────────────┘
txt └─────┘ └──────────────────────────┘
par └─────┘ └──────────────────────────┘
pid ┴ └──────────────────────────┘
st ──────────────────────────────────────┘└─
72 rw [sS, tT, sInter_union_sInter],
id └┘ └┘ └─────────────────┘
src └──┘ └┘ └┘└─────────────────┘┴
typ └──┘└┘└┘└┘└┘└─────────────────┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ───────┘└──┘└───────────────────┘└──
73 apply is_Gδ_bInter_of_open (countable_prod Scount Tcount),
id └──────────────────┘ └────────────┘ └────┘ └────┘
src └────┘└──────────────────┘┴ └────────────┘┴ ┴ ┴
typ └────┘└──────────────────┘┴ └────────────┘┴└────┘┴└────┘┴
doc └────┘ ┴ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────┘└─
74 rintros ⟨a, b⟩ hab,
src └────────────────┘
typ └────────────────┘
doc └────────────────┘
txt └────────────────┘
par └────────────────┘
pid └─────────┘
st ───────────────────┘└─
75 simp only [set.prod_mk_mem_set_prod_eq] at hab,
id └─────────────────────────┘
src └─────────┘└─────────────────────────┘└──────┘
typ └─────────┘└─────────────────────────┘└──────┘
doc └─────────┘ └──────┘
txt └─────────┘ └──────┘
par └─────────┘ └──────┘
pid ┴└──┘└┘ ┴┴└────┘
st ───────────────────────────────────────────────┘└─
76 have aopen : is_open a := Sopen a hab.1,
id └─────┘ ┴ └───┘ ┴ └─┘
src └───────────┘└─────┘┴ └──┘ ┴ ┴ └┘
typ └───────────┘└─────┘┴┴└──┘└───┘┴┴┴└─┘└┘
doc └───────────┘└─────┘┴ └──┘ ┴ ┴ └┘
txt └───────────┘ ┴ └──┘ ┴ ┴ └┘
par └───────────┘ ┴ └──┘ ┴ ┴ └┘
pid └────────┘└─┘ ┴ └──┘ ┴ ┴ └┘
st ────────────────────────────────────────┘└─
77 have bopen : is_open b := Topen b hab.2,
id └─────┘ ┴ └───┘ ┴ └─┘
src └───────────┘└─────┘┴ └──┘ ┴ ┴ └┘
typ └───────────┘└─────┘┴┴└──┘└───┘┴┴┴└─┘└┘
doc └───────────┘└─────┘┴ └──┘ ┴ ┴ └┘
txt └───────────┘ ┴ └──┘ ┴ ┴ └┘
par └───────────┘ ┴ └──┘ ┴ ┴ └┘
pid └────────┘└─┘ ┴ └──┘ ┴ ┴ └┘
st ────────────────────────────────────────┘└─
78 simp [aopen, bopen, is_open_union]
id └───┘ └───┘ └───────────┘
src └────┘ └┘ └┘└───────────┘└┘
typ └────┘└───┘└┘└───┘└┘└───────────┘└┘
doc └────┘ └┘ └┘ └┘
txt └────┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘
pid ┴┴ └┘ └┘ ┴┴
st ────────────────────────────────────┘
79 end
st └─┘
80
81 end is_Gδ
82
83 section Baire_theorem
84 open metric
85 variables [metric_space α] [complete_space α]
id └──────────┘ └────────────┘
src └──────────┘ └────────────┘
typ └──────────┘ └────────────┘
doc └──────────┘ └────────────┘
86
87 /-- Baire theorem: a countable intersection of dense open sets is dense. Formulated here when
88 the source space is ℕ (and subsumed below by `dense_Inter_of_open` working with any
89 encodable source space). -/
90 theorem dense_Inter_of_open_nat {f : ℕ → set α} (ho : ∀n, is_open (f n))
id ┴ └─┘ ┴ ┴ └─────┘ ┴ ┴
src ┴ └─┘ └─────┘
typ ┴ └─┘ ┴ ┴ └─────┘ ┴ ┴
doc └─────┘
91 (hd : ∀n, closure (f n) = univ) : closure (⋂n, f n) = univ :=
id ┴ └─────┘ ┴ ┴ ┴ └──┘ └─────┘ ┴┴┴ ┴ ┴ ┴ └──┘
src └─────┘ ┴ └──┘ └─────┘ ┴ ┴ ┴ └──┘
typ ┴ └─────┘ ┴ ┴ ┴ └──┘ └─────┘ ┴┴┴ ┴ ┴ ┴ └──┘
doc └─────┘ └─────┘ ┴ ┴
92 begin
st └─────
93 let B : ℕ → ℝ := λn, ((1/2)^n : ℝ),
id ┴ ┴ ┴
src └──────┘ ┴ ┴┴└──┘ └─┘ ┴┴└┘┴ └─┘ ┴
typ └──────┘ ┴ ┴┴└──┘ └─┘ ┴┴└┘┴ └─┘ ┴
doc └──────┘ ┴ ┴ └──┘ └─┘ ┴ └┘ └─┘ ┴
txt └──────┘ ┴ ┴ └──┘ └─┘ ┴ └┘ └─┘ ┴
par └──────┘ ┴ ┴ └──┘ └─┘ ┴ └┘ └─┘ ┴
pid └───┘└─┘ ┴ ┴ └──┘ └─┘ ┴ └┘ └─┘ ┴
st ───────────────────────────────────┘└─
94 have Bpos : ∀n, 0 < B n := λn, begin apply pow_pos, by norm_num end,
id ┴ ┴ └─────┘
src └──────────┘ ┴ └─┘┴┴ ┴ └──┘ └─┘ ┴└────┘└─────┘└───┘└───────┘└─┘
typ └──────────┘ ┴ └─┘┴┴┴┴ └──┘ └─┘ ┴└────┘└─────┘└───┘└───────┘└─┘
doc └──────────┘ ┴ └─┘ ┴ ┴ └──┘ └─┘ ┴└────┘ └───┘└───────┘└─┘
txt └──────────┘ ┴ └─┘ ┴ ┴ └──┘ └─┘ ┴└────┘ └───┘└───────┘└─┘
par └──────────┘ ┴ └─┘ ┴ ┴ └──┘ └─┘ ┴└────┘ └───┘└───────┘└─┘
pid └───────┘└─┘ ┴ └─┘ ┴ ┴ └──┘ └─┘ └─────┘ └───────────────┘
st ────────────────────────────────┘└─────────────────┘ └─┘└─
95 /- Translate the density assumption into two functions `center` and `radius` associating
st ───────────────────────────────────────────────────────────────────────────────────────────
96 to any n, x, δ, δpos a center and a positive radius such that
st ────────────────────────────────────────────────────────────────
97 `closed_ball center radius` is included both in `f n` and in `closed_ball x δ`.
st ──────────────────────────────────────────────────────────────────────────────────
98 We can also require `radius ≤ (1/2)^(n+1), to ensure we get a Cauchy sequence later. -/
st ──────────────────────────────────────────────────────────────────────────────────────────
99 have : ∀n x δ, ∃y r, δ > 0 → (r > 0 ∧ r ≤ B (n+1) ∧ closed_ball y r ⊆ (closed_ball x δ) ∩ f n),
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴
src └─────┘ └───┘ ┴┴└─┘┴┴ ┴┴└─┘ ┴ ┴ └─┘┴┴ ┴┴┴ ┴ ┴└─┘ ┴ ┴ ┴ ┴┴┴ └─────────┘┴ ┴ └┘┴┴ ┴ ┴
typ └─────┘ └───┘ ┴┴└─┘┴┴ ┴┴└─┘ ┴ ┴ └─┘┴┴ ┴┴┴┴┴ ┴└─┘ ┴ ┴ ┴ ┴┴┴ └─────────┘┴ ┴ └┘┴┴┴┴ ┴
doc └─────┘ └───┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─────────┘┴ ┴ └┘ ┴ ┴ ┴
txt └─────┘ └───┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
par └─────┘ └───┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
pid └───┘└┘ └───┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────────────────────────────────────┘└─
100 { assume n x δ,
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid └──────────┘
st ───┘└──────────┘└─
101 by_cases δpos : δ > 0,
id ┴
src └───────┘ └─┘ ┴ └┘
typ └───────┘ └─┘┴┴ └┘
doc └───────┘ └─┘ ┴ └┘
txt └───────┘ └─┘ ┴ └┘
par └───────┘ └─┘ ┴ └┘
pid ┴ └─┘ ┴ ┴┴
st ────────────────────────┘└─
102 { have : x ∈ closure (f n) := by simpa only [(hd n).symm] using mem_univ x,
id ┴ ┴ └─────┘ ┴ ┴ └┘ ┴ └──────┘ ┴
src └─────┘ ┴┴┴└─────┘┴ ┴ └───┘ ┴└──────────┘ ┴ └────────────┘└──────┘┴
typ └─────┘┴┴┴┴└─────┘┴ ┴┴┴└───┘ ┴└──────────┘ └┘┴┴└────────────┘└──────┘┴┴
doc └─────┘ ┴ ┴└─────┘┴ ┴ └───┘ ┴└──────────┘ ┴ └────────────┘ ┴
txt └─────┘ ┴ ┴ ┴ ┴ └───┘ ┴└──────────┘ ┴ └────────────┘ ┴
par └─────┘ ┴ ┴ ┴ ┴ └───┘ ┴└──────────┘ ┴ └────────────┘ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴└──┘ └───────────┘ ┴ └────────────┘ ┴
st ─────┘└────────────────────────────┘└────────────────────────────────────────┘└─
103 rcases mem_closure_iff'.1 this (δ/2) (half_pos δpos) with ⟨y, ys, xy⟩,
id └──────────────┘ └──┘ ┴ └──────┘ └──┘
src └─────┘└──────────────┘└─┘ ┴ └─┘ └──────┘┴ └────────────────┘
typ └─────┘└──────────────┘└─┘└──┘┴ ┴ └─┘ └──────┘┴└──┘└────────────────┘
doc └─────┘└──────────────┘└─┘ ┴ └─┘ ┴ └────────────────┘
txt └─────┘ └─┘ ┴ └─┘ ┴ └────────────────┘
par └─────┘ └─┘ ┴ └─┘ ┴ └────────────────┘
pid ┴ └─┘ ┴ └─┘ ┴ └────────────────┘
st ──────────────────────────────────────────────────────────────────────────┘└─
104 rw dist_comm at xy,
id └───────┘
src └─┘└───────┘└────┘
typ └─┘└───────┘└────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ └────┘
st ───────────────────────┘└─
105 rcases is_open_iff.1 (ho n) y ys with ⟨r, rpos, hr⟩,
id └─────────┘ └┘ ┴ ┴ └┘
src └─────┘└─────────┘└─┘ ┴ └┘ ┴ └─────────────────┘
typ └─────┘└─────────┘└─┘ └┘┴┴└┘┴┴└┘└─────────────────┘
doc └─────┘ └─┘ ┴ └┘ ┴ └─────────────────┘
txt └─────┘ └─┘ ┴ └┘ ┴ └─────────────────┘
par └─────┘ └─┘ ┴ └┘ ┴ └─────────────────┘
pid ┴ └─┘ ┴ └┘ ┴ └─────────────────┘
st ────────────────────────────────────────────────────────┘└─
106 refine ⟨y, min (min (δ/2) (r/2)) (B (n+1)), λ_, ⟨_, _, λz hz, ⟨_, _⟩⟩⟩,
id ┴ └─┘ ┴ ┴ ┴ ┴
src └─────┘ └┘ ┴ └─┘┴ └─┘ └──┘ ┴ └───┘ └─┘ └────┘ └────┘ └─────┘
typ └─────┘ ┴└┘ ┴ └─┘┴ ┴ └─┘ ┴ └──┘ ┴┴ ┴ └───┘ └─┘ └────┘ └────┘ └─────┘
doc └─────┘ └┘ ┴ ┴ └─┘ └──┘ ┴ └───┘ └─┘ └────┘ └────┘ └─────┘
txt └─────┘ └┘ ┴ ┴ └─┘ └──┘ ┴ └───┘ └─┘ └────┘ └────┘ └─────┘
par └─────┘ └┘ ┴ ┴ └─┘ └──┘ ┴ └───┘ └─┘ └────┘ └────┘ └─────┘
pid ┴ └┘ ┴ ┴ └─┘ └──┘ ┴ └───┘ └─┘ └────┘ └────┘ └─────┘
st ───────────────────────────────────────────────────────────────────────────┘└─
107 show 0 < min (min (δ / 2) (r/2)) (B (n+1)),
id └─┘ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ └─┘┴ ┴ └──┘ └──┘ ┴ └─┘
typ └─────┘ ┴ ┴ └─┘┴ ┴┴ └──┘ ┴ └──┘ ┴┴ ┴ └─┘
doc └─────┘ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ └─┘
txt └─────┘ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ └─┘
par └─────┘ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ └─┘
pid └─────┘ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ └─┘
st ───────────────────────────────────────────────┘└─
108 from lt_min (lt_min (half_pos δpos) (half_pos rpos)) (Bpos (n+1)),
id └────┘ └──┘ └──────┘ └──┘ └──┘ ┴
src └───┘ ┴ └────┘┴ ┴ └┘ └──────┘┴ └─┘ ┴ └─┘
typ └───┘ ┴ └────┘┴ ┴└──┘└┘ └──────┘┴└──┘└─┘ └──┘┴ ┴ └─┘
doc └───┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ └─┘
txt └───┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ └─┘
par └───┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ └─┘
pid └───┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ └─┘
st ────────────────────────────────────────────────────────────────────────┘└─
109 show min (min (δ / 2) (r/2)) (B (n+1)) ≤ B (n+1), from min_le_right _ _,
id └─┘ ┴ ┴ ┴ ┴ └──────────┘
src └───┘ ┴ └─┘┴ ┴ └──┘ └──┘ ┴ └──┘ ┴ ┴ └┘ └───┘└──────────┘└──┘
typ └───┘ ┴ └─┘┴ ┴┴ └──┘ ┴ └──┘ ┴ └──┘ ┴┴┴ ┴ └┘ └───┘└──────────┘└──┘
doc └───┘ ┴ ┴ ┴ └──┘ └──┘ ┴ └──┘ ┴ ┴ └┘ └───┘ └──┘
txt └───┘ ┴ ┴ ┴ └──┘ └──┘ ┴ └──┘ ┴ ┴ └┘ └───┘ └──┘
par └───┘ ┴ ┴ ┴ └──┘ └──┘ ┴ └──┘ ┴ ┴ └┘ └───┘ └──┘
pid └───┘ ┴ ┴ ┴ └──┘ └──┘ ┴ └──┘ ┴ ┴ └┘ └───┘ └──┘
st ────────────────────────────────────────────────────────────────────────────┘└─
110 show z ∈ closed_ball x δ, from calc
id ┴ └─────────┘ ┴ ┴
src └───┘ ┴ ┴└─────────┘┴ ┴ └───┘ └
typ └───┘┴┴ ┴└─────────┘┴┴┴┴ └───┘ └
doc └───┘ ┴ ┴└─────────┘┴ ┴ └───┘ └
txt └───┘ ┴ ┴ ┴ ┴ └───┘ └
par └───┘ ┴ ┴ ┴ ┴ └───┘ └
pid └───┘ ┴ ┴ ┴ ┴ └───┘ └
st ──────────────────────────────────────────
111 dist z x ≤ dist z y + dist y x : dist_triangle _ _ _
id ┴ └──┘ ┴ ┴ └───────────┘
src ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘┴ ┴ └─┘└───────────┘└──────
typ ───────┘ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴└──┘┴┴┴┴└─┘└───────────┘└──────
doc ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──────
txt ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──────
par ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──────
pid ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──────
st ─────────────────────────────────────────────────────────────
112 ... ≤ (min (min (δ / 2) (r/2)) (B (n+1))) + (δ/2) : add_le_add hz (le_of_lt xy)
id └─┘ ┴ ┴ ┴ ┴ └┘ └──────┘ └┘
src ───────────┘ ┴ ┴ └─┘┴ ┴ └──┘ └──┘ ┴ └───┘ ┴ └───┘ ┴ ┴ └──────┘┴ └─
typ ───────────┘ ┴ ┴ └─┘┴ ┴ └──┘ ┴ └──┘ ┴┴ ┴ └───┘ ┴ ┴ └───┘ ┴└┘┴ └──────┘┴└┘└─
doc ───────────┘ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ └───┘ ┴ └───┘ ┴ ┴ ┴ └─
txt ───────────┘ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ └───┘ ┴ └───┘ ┴ ┴ ┴ └─
par ───────────┘ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ └───┘ ┴ └───┘ ┴ ┴ ┴ └─
pid ───────────┘ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ └───┘ ┴ └───┘ ┴ ┴ ┴ └─
st ────────────────────────────────────────────────────────────────────────────────────────
113 ... ≤ δ/2 + δ/2 : add_le_add (le_trans (min_le_left _ _) (min_le_left _ _)) (le_refl _)
id └────────┘ └──────┘ └─────────┘ └─────┘
src ───────────┘ ┴ └┘ ┴ └──┘└────────┘┴ └──────┘┴ └────┘ └─────────┘└─────┘ └─────┘└───
typ ───────────┘ ┴ └┘ ┴ └──┘└────────┘┴ └──────┘┴ └────┘ └─────────┘└─────┘ └─────┘└───
doc ───────────┘ ┴ └┘ ┴ └──┘ ┴ ┴ └────┘ └─────┘ └───
txt ───────────┘ ┴ └┘ ┴ └──┘ ┴ ┴ └────┘ └─────┘ └───
par ───────────┘ ┴ └┘ ┴ └──┘ ┴ ┴ └────┘ └─────┘ └───
pid ───────────┘ ┴ └┘ ┴ └──┘ ┴ ┴ └────┘ └─────┘ └───
st ────────────────────────────────────────────────────────────────────────────────────────────────
114 ... = δ : add_halves _,
id └────────┘
src ───────────┘ ┴ └─┘└────────┘└┘
typ ───────────┘ ┴ └─┘└────────┘└┘
doc ───────────┘ ┴ └─┘ └┘
txt ───────────┘ ┴ └─┘ └┘
par ───────────┘ ┴ └─┘ └┘
pid ───────────┘ ┴ └─┘ └┘
st ─────────────────────────────┘└─
115 show z ∈ f n, from hr (calc
id ┴ ┴ ┴ └┘
src └───┘ ┴ ┴ ┴ └───┘ ┴ └
typ └───┘┴┴ ┴┴┴┴ └───┘└┘┴ └
doc └───┘ ┴ ┴ ┴ └───┘ ┴ └
txt └───┘ ┴ ┴ ┴ └───┘ ┴ └
par └───┘ ┴ ┴ ┴ └───┘ ┴ └
pid └───┘ ┴ ┴ ┴ └───┘ ┴ └
st ──────────────────────────────────
116 dist z y ≤ min (min (δ / 2) (r/2)) (B (n+1)) : hz
id └──┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘
src ───────┘└──┘┴ ┴ ┴ ┴ ┴ └─┘┴ ┴ └──┘ └──┘ ┴ └────┘ └
typ ───────┘└──┘┴┴┴┴┴ ┴ ┴ └─┘┴ ┴┴ └──┘ ┴ └──┘ ┴┴ ┴ └────┘└┘└
doc ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ └────┘ └
txt ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ └────┘ └
par ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ └────┘ └
pid ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └──┘ ┴ └────┘ └
st ──────────────────────────────────────────────────────────
117 ... ≤ r/2 : le_trans (min_le_left _ _) (min_le_right _ _)
id └──────┘ └─────────┘ └──────────┘
src ───────────┘ ┴ └──┘└──────┘┴ └─────────┘└────┘ └──────────┘└─────
typ ───────────┘ ┴ └──┘└──────┘┴ └─────────┘└────┘ └──────────┘└─────
doc ───────────┘ ┴ └──┘ ┴ └────┘ └─────
txt ───────────┘ ┴ └──┘ ┴ └────┘ └─────
par ───────────┘ ┴ └──┘ ┴ └────┘ └─────
pid ───────────┘ ┴ └──┘ ┴ └────┘ └─────
st ──────────────────────────────────────────────────────────────────
118 ... < r : half_lt_self rpos) },
id └──────────┘ └──┘
src ───────────┘ ┴ └─┘└──────────┘┴ └┘
typ ───────────┘ ┴ └─┘└──────────┘┴└──┘└┘
doc ───────────┘ ┴ └─┘ ┴ └┘
txt ───────────┘ ┴ └─┘ ┴ └┘
par ───────────┘ ┴ └─┘ ┴ └┘
pid ───────────┘ ┴ └─┘ ┴ ┴┴
st ────────────────────────────────────┘└┘└
119 { use [x, 0] }},
id ┴
src └───┘ └───┘
typ └───┘┴└───┘
doc └───┘ └───┘
txt └───┘ └───┘
par └───┘ └───┘
pid └┘ └──┘┴
st ────────────────┘└─┘└
120 choose center radius H using this,
id └──┘
src └───────────────────────────┘
typ └───────────────────────────┘└──┘
doc └───────────────────────────┘
txt └───────────────────────────┘
par └───────────────────────────┘
pid └─────┘└───────┘└─────┘
st ──────────────────────────────────┘└─
121
st ─
122 refine subset.antisymm (subset_univ _) (λx hx, _),
id └─────────────┘ └─────────┘
src └─────┘└─────────────┘┴ └─────────┘└──┘ └──────┘
typ └─────┘└─────────────┘┴ └─────────┘└──┘ └──────┘
doc └─────┘ ┴ └──┘ └──────┘
txt └─────┘ ┴ └──┘ └──────┘
par └─────┘ ┴ └──┘ └──────┘
pid ┴ ┴ └──┘ └──────┘
st ──────────────────────────────────────────────────┘└─
123 refine metric.mem_closure_iff'.2 (λε εpos, _),
id └─────────────────────┘
src └─────┘└─────────────────────┘└─┘ └────────┘
typ └─────┘└─────────────────────┘└─┘ └────────┘
doc └─────┘└─────────────────────┘└─┘ └────────┘
txt └─────┘ └─┘ └────────┘
par └─────┘ └─┘ └────────┘
pid ┴ └─┘ └────────┘
st ──────────────────────────────────────────────┘└─
124 /- ε is positive. We have to find a point in the ball of radius ε around x belonging to all `f n`.
st ─────────────────────────────────────────────────────────────────────────────────────────────────────
125 For this, we construct inductively a sequence `F n = (c n, r n)` such that the closed ball
st ─────────────────────────────────────────────────────────────────────────────────────────────
126 `closed_ball (c n) (r n)` is included in the previous ball and in `f n`, and such that
st ─────────────────────────────────────────────────────────────────────────────────────────
127 `r n` is small enough to ensure that `c n` is a Cauchy sequence. Then `c n` converges to a
st ─────────────────────────────────────────────────────────────────────────────────────────────
128 limit which belongs to all the `f n`. -/
st ───────────────────────────────────────────
129 let F : ℕ → (α × ℝ) := λn, nat.rec_on n (prod.mk x (min (ε/2) 1))
id ┴ ┴ └────────┘ ┴ └─┘ ┴
src └──────┘ ┴ ┴ ┴┴┴ └───┘ └─┘└────────┘┴ ┴ ┴ ┴ └─┘┴ └──────
typ └──────┘ ┴ ┴ ┴┴┴┴ └───┘ └─┘└────────┘┴ ┴ ┴┴┴ └─┘┴ ┴ └──────
doc └──────┘ ┴ ┴ ┴ ┴ └───┘ └─┘ ┴ ┴ ┴ ┴ ┴ └──────
txt └──────┘ ┴ ┴ ┴ ┴ └───┘ └─┘ ┴ ┴ ┴ ┴ ┴ └──────
par └──────┘ ┴ ┴ ┴ ┴ └───┘ └─┘ ┴ ┴ ┴ ┴ ┴ └──────
pid └───┘└─┘ ┴ ┴ ┴ ┴ ┴└──┘ └─┘ ┴ ┴ ┴ ┴ ┴ └──────
st ────────────────────────────────────────────────────────────────────
130 (λn p, prod.mk (center n p.1 p.2) (radius n p.1 p.2)),
id └─────┘ └────┘ └────┘
src ─────────────────────────────┘ └───┘└─────┘┴ ┴ ┴ └─┘ └──┘ ┴ ┴ └─┘ └──┘
typ ─────────────────────────────┘ └───┘└─────┘┴ └────┘┴ ┴ └─┘ └──┘ └────┘┴ ┴ └─┘ └──┘
doc ─────────────────────────────┘ └───┘ ┴ ┴ ┴ └─┘ └──┘ ┴ ┴ └─┘ └──┘
txt ─────────────────────────────┘ └───┘ ┴ ┴ ┴ └─┘ └──┘ ┴ ┴ └─┘ └──┘
par ─────────────────────────────┘ └───┘ ┴ ┴ ┴ └─┘ └──┘ ┴ ┴ └─┘ └──┘
pid ─────────────────────────────┘ └───┘ ┴ ┴ ┴ └─┘ └──┘ ┴ ┴ └─┘ └──┘
st ──────────────────────────────────────────────────────────────────────────────────┘└─
131 let c : ℕ → α := λn, (F n).1,
id ┴ ┴
src └──────┘ ┴ ┴ └──┘ └─┘ ┴ └─┘
typ └──────┘ ┴ ┴┴└──┘ └─┘ ┴┴ └─┘
doc └──────┘ ┴ ┴ └──┘ └─┘ ┴ └─┘
txt └──────┘ ┴ ┴ └──┘ └─┘ ┴ └─┘
par └──────┘ ┴ ┴ └──┘ └─┘ ┴ └─┘
pid └───┘└─┘ ┴ ┴ └──┘ └─┘ ┴ ┴└┘
st ─────────────────────────────┘└─
132 let r : ℕ → ℝ := λn, (F n).2,
id ┴
src └──────┘ ┴ ┴ └──┘ └─┘ ┴ └─┘
typ └──────┘ ┴ ┴ └──┘ └─┘ ┴┴ └─┘
doc └──────┘ ┴ ┴ └──┘ └─┘ ┴ └─┘
txt └──────┘ ┴ ┴ └──┘ └─┘ ┴ └─┘
par └──────┘ ┴ ┴ └──┘ └─┘ ┴ └─┘
pid └───┘└─┘ ┴ ┴ └──┘ └─┘ ┴ ┴└┘
st ─────────────────────────────┘└─
133 have rpos : ∀n, r n > 0,
id ┴
src └──────────┘ ┴ ┴ ┴ ┴ └┘
typ └──────────┘ ┴ ┴┴┴ ┴ └┘
doc └──────────┘ ┴ ┴ ┴ ┴ └┘
txt └──────────┘ ┴ ┴ ┴ ┴ └┘
par └──────────┘ ┴ ┴ ┴ ┴ └┘
pid └───────┘└─┘ ┴ ┴ ┴ ┴ ┴┴
st ────────────────────────┘└─
134 { assume n,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───┘└──────┘└─
135 induction n with n hn,
id ┴
src └────────┘ └────────┘
typ └────────┘┴└────────┘
doc └────────┘ └────────┘
txt └────────┘ └────────┘
par └────────┘ └────────┘
pid ┴ ┴└───────┘
st ────────────────────────┘└─
136 exact lt_min (half_pos εpos) (zero_lt_one),
id └────┘ └──────┘ └──┘ └─────────┘
src └────┘└────┘┴ └──────┘┴ └┘ └─────────┘┴
typ └────┘└────┘┴ └──────┘┴└──┘└┘ └─────────┘┴
doc └────┘ ┴ ┴ └┘ ┴
txt └────┘ ┴ ┴ └┘ ┴
par └────┘ ┴ ┴ └┘ ┴
pid ┴ ┴ ┴ └┘ ┴
st ─────────────────────────────────────────────┘└─
137 exact (H n (c n) (r n) hn).1 },
id ┴ ┴ ┴ ┴ └┘
src └────┘ ┴ ┴ ┴ └┘ ┴ └┘ └──┘
typ └────┘ ┴┴ ┴ ┴┴ └┘ ┴┴┴└┘└┘└──┘
doc └────┘ ┴ ┴ ┴ └┘ ┴ └┘ └──┘
txt └────┘ ┴ ┴ ┴ └┘ ┴ └┘ └──┘
par └────┘ ┴ ┴ ┴ └┘ ┴ └┘ └──┘
pid ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴└─┘
st ────────────────────────────────┘└┘└
138 have rB : ∀n, r n ≤ B n,
id ┴ ┴
src └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └────────┘ ┴ ┴┴┴ ┴ ┴┴┴
doc └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
txt └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
par └────────┘ ┴ ┴ ┴ ┴ ┴ ┴
pid └─────┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴
st ────────────────────────┘└─
139 { assume n,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───┘└──────┘└─
140 induction n with n hn,
id ┴
src └────────┘ └────────┘
typ └────────┘┴└────────┘
doc └────────┘ └────────┘
txt └────────┘ └────────┘
par └────────┘ └────────┘
pid ┴ ┴└───────┘
st ────────────────────────┘└─
141 exact min_le_right _ _,
id └──────────┘
src └────┘└──────────┘└──┘
typ └────┘└──────────┘└──┘
doc └────┘ └──┘
txt └────┘ └──┘
par └────┘ └──┘
pid ┴ └──┘
st ─────────────────────────┘└─
142 exact (H n (c n) (r n) (rpos n)).2.1 },
id ┴ ┴ ┴ └──┘ ┴
src └────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └─────┘
typ └────┘ ┴┴ ┴ ┴┴ └┘ ┴┴ └┘ └──┘┴┴└─────┘
doc └────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └─────┘
txt └────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └─────┘
par └────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └─────┘
pid ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └──┘└─┘
st ────────────────────────────────────────┘└┘└
143 have incl : ∀n, closed_ball (c (n+1)) (r (n+1)) ⊆ (closed_ball (c n) (r n)) ∩ (f n) :=
id └─────────┘ ┴ ┴ ┴
src └──────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └──┘ ┴ └─────────┘┴ ┴ └┘ ┴ └─┘ ┴ ┴ └────
typ └──────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └──┘ ┴ └─────────┘┴ ┴┴ └┘ ┴┴ └─┘ ┴ ┴┴ └────
doc └──────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └──┘ ┴ └─────────┘┴ ┴ └┘ ┴ └─┘ ┴ ┴ └────
txt └──────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ └────
par └──────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ └────
pid └───────┘└─┘ ┴ ┴ ┴ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴└───
st ─────────────────────────────────────────────────────────────────────────────────────────
144 λn, (H n (c n) (r n) (rpos n)).2.2,
id ┴ ┴ ┴ └──┘
src ───┘ └─┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └────┘
typ ───┘ └─┘ ┴┴ ┴ ┴┴ └┘ ┴┴ └┘ └──┘┴ └────┘
doc ───┘ └─┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └────┘
txt ───┘ └─┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └────┘
par ───┘ └─┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └────┘
pid ───┘ └─┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └──┘└┘
st ─────────────────────────────────────┘└─
145 have cdist : ∀n, dist (c n) (c (n+1)) ≤ B n,
id └──┘ ┴ ┴
src └───────────┘ ┴ ┴└──┘┴ ┴ └┘ ┴ └──┘ ┴ ┴
typ └───────────┘ ┴ ┴└──┘┴ ┴ └┘ ┴┴ └──┘ ┴┴┴
doc └───────────┘ ┴ ┴ ┴ ┴ └┘ ┴ └──┘ ┴ ┴
txt └───────────┘ ┴ ┴ ┴ ┴ └┘ ┴ └──┘ ┴ ┴
par └───────────┘ ┴ ┴ ┴ ┴ └┘ ┴ └──┘ ┴ ┴
pid └────────┘└─┘ ┴ ┴ ┴ ┴ └┘ ┴ └──┘ ┴ ┴
st ────────────────────────────────────────────┘└─
146 { assume n,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───┘└──────┘└─
147 rw dist_comm,
id └───────┘
src └─┘└───────┘
typ └─┘└───────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────────┘└─
148 have A : c (n+1) ∈ closed_ball (c (n+1)) (r (n+1)) :=
id └─────────┘ ┴ ┴ ┴
src └───────┘ ┴ └─┘ ┴└─────────┘┴ ┴ └──┘ ┴ └──────
typ └───────┘ ┴ └─┘ ┴└─────────┘┴ ┴┴ └──┘ ┴┴ ┴ └──────
doc └───────┘ ┴ └─┘ ┴└─────────┘┴ ┴ └──┘ ┴ └──────
txt └───────┘ ┴ └─┘ ┴ ┴ ┴ └──┘ ┴ └──────
par └───────┘ ┴ └─┘ ┴ ┴ ┴ └──┘ ┴ └──────
pid └────┘└─┘ ┴ └─┘ ┴ ┴ ┴ └──┘ ┴ └─┘└───
st ──────────────────────────────────────────────────────────
149 mem_closed_ball_self (le_of_lt (rpos (n+1))),
id └──────────────────┘ └──────┘ └──┘ ┴
src ─────┘└──────────────────┘┴ └──────┘┴ ┴ └──┘
typ ─────┘└──────────────────┘┴ └──────┘┴ └──┘┴ ┴ └──┘
doc ─────┘ ┴ ┴ ┴ └──┘
txt ─────┘ ┴ ┴ ┴ └──┘
par ─────┘ ┴ ┴ ┴ └──┘
pid ─────┘ ┴ ┴ ┴ └──┘
st ─────────────────────────────────────────────────┘└─
150 have I := calc
src └────────┘ └
typ └────────┘ └
doc └────────┘ └
txt └────────┘ └
par └────────┘ └
pid └────┘┴└─┘ └
st ───────────────────
151 closed_ball (c (n+1)) (r (n+1)) ⊆ closed_ball (c n) (r n) :
id ┴
src ─────┘ ┴ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ └───
typ ─────┘ ┴ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ └┘ ┴┴ └───
doc ─────┘ ┴ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ └───
txt ─────┘ ┴ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ └───
par ─────┘ ┴ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ └───
pid ─────┘ ┴ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ └───
st ──────────────────────────────────────────────────────────────────
152 subset.trans (incl n) (inter_subset_left _ _)
id └──────────┘ └──┘ └───────────────┘
src ───────┘└──────────┘┴ ┴ └┘ └───────────────┘└─────
typ ───────┘└──────────┘┴ └──┘┴ └┘ └───────────────┘└─────
doc ───────┘ ┴ ┴ └┘ └─────
txt ───────┘ ┴ ┴ └┘ └─────
par ───────┘ ┴ ┴ └┘ └─────
pid ───────┘ ┴ ┴ └┘ └─────
st ──────────────────────────────────────────────────────
153 ... ⊆ closed_ball (c n) (B n) : closed_ball_subset_closed_ball (rB n),
id └─────────┘ ┴ ┴ └────────────────────────────┘ └┘ ┴
src ─────────┘ ┴└─────────┘┴ ┴ └┘ ┴ └──┘└────────────────────────────┘┴ ┴ ┴
typ ─────────┘ ┴└─────────┘┴ ┴┴ └┘ ┴┴ └──┘└────────────────────────────┘┴ └┘┴┴┴
doc ─────────┘ ┴└─────────┘┴ ┴ └┘ ┴ └──┘ ┴ ┴ ┴
txt ─────────┘ ┴ ┴ ┴ └┘ ┴ └──┘ ┴ ┴ ┴
par ─────────┘ ┴ ┴ ┴ └┘ ┴ └──┘ ┴ ┴ ┴
pid ─────────┘ ┴ ┴ ┴ └┘ ┴ └──┘ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────────────────┘└─
154 exact I A },
id ┴ ┴
src └────┘ ┴ ┴
typ └────┘┴┴┴┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ─────────────┘└┘└
155 have : cauchy_seq c,
id └────────┘ ┴
src └─────┘└────────┘┴
typ └─────┘└────────┘┴┴
doc └─────┘└────────┘┴
txt └─────┘ ┴
par └─────┘ ┴
pid └───┘└┘ ┴
st ────────────────────┘└─
156 { refine cauchy_seq_of_le_geometric (1/2) 1 (by norm_num) (λn, _),
id └────────────────────────┘
src └─────┘└────────────────────────┘┴ ┴ └───┘ ┴└──────┘└┘ └───┘
typ └─────┘└────────────────────────┘┴ ┴ └───┘ ┴└──────┘└┘ └───┘
doc └─────┘└────────────────────────┘┴ ┴ └───┘ ┴└──────┘└┘ └───┘
txt └─────┘ ┴ ┴ └───┘ ┴└──────┘└┘ └───┘
par └─────┘ ┴ ┴ └───┘ ┴└──────┘└┘ └───┘
pid ┴ ┴ ┴ └───┘ └─────────┘ └───┘
st ───┘└───────────────────────────────────────────┘└───────┘└───────┘└─
157 rw one_mul,
id └─────┘
src └─┘└─────┘
typ └─┘└─────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────────────┘└─
158 exact cdist n },
id └───┘ ┴
src └────┘ ┴ ┴
typ └────┘└───┘┴┴┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ─────────────────┘└┘└
159 -- as the sequence `c n` is Cauchy in a complete space, it converges to a limit `y`.
st ───────────────────────────────────────────────────────────────────────────────────────
160 rcases cauchy_seq_tendsto_of_complete this with ⟨y, ylim⟩,
id └────────────────────────────┘ └──┘
src └─────┘└────────────────────────────┘┴ └─────────────┘
typ └─────┘└────────────────────────────┘┴└──┘└─────────────┘
doc └─────┘└────────────────────────────┘┴ └─────────────┘
txt └─────┘ ┴ └─────────────┘
par └─────┘ ┴ └─────────────┘
pid ┴ ┴ └─────────────┘
st ──────────────────────────────────────────────────────────┘└─
161 -- this point `y` will be the desired point. We will check that it belongs to all
st ────────────────────────────────────────────────────────────────────────────────────
162 -- `f n` and to `ball x ε`.
st ──────────────────────────────
163 use y,
id ┴
src └──┘
typ └──┘┴
doc └──┘
txt └──┘
par └──┘
pid ┴
st ──────┘└─
164 simp only [exists_prop, set.mem_Inter],
id └─────────┘ └───────────┘
src └─────────┘└─────────┘└┘└───────────┘┴
typ └─────────┘└─────────┘└┘└───────────┘┴
doc └─────────┘ └┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st ───────────────────────────────────────┘└─
165 have I : ∀n, ∀m ≥ n, closed_ball (c m) (r m) ⊆ closed_ball (c n) (r n),
id └─────────┘ ┴ ┴
src └───────┘ ┴ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴└─────────┘┴ ┴ └┘ ┴ ┴
typ └───────┘ ┴ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴└─────────┘┴ ┴┴ └┘ ┴┴ ┴
doc └───────┘ ┴ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴└─────────┘┴ ┴ └┘ ┴ ┴
txt └───────┘ ┴ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴
par └───────┘ ┴ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴
pid └────┘└─┘ ┴ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴
st ───────────────────────────────────────────────────────────────────────┘└─
166 { assume n,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───┘└──────┘└─
167 refine nat.le_induction _ (λm hnm h, _),
id └──────────────┘
src └─────┘└──────────────┘└─┘ └─────────┘
typ └─────┘└──────────────┘└─┘ └─────────┘
doc └─────┘└──────────────┘└─┘ └─────────┘
txt └─────┘ └─┘ └─────────┘
par └─────┘ └─┘ └─────────┘
pid ┴ └─┘ └─────────┘
st ──────────────────────────────────────────┘└─
168 { exact subset.refl _ },
id └─────────┘
src └────┘└─────────┘└─┘
typ └────┘└─────────┘└─┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └┘┴
st ─────┘└──────────────────┘└┘└
169 { exact subset.trans (incl m) (subset.trans (inter_subset_left _ _) h) }},
id └──┘ ┴ └──────────┘ └───────────────┘ ┴
src └────┘ ┴ ┴ └┘ └──────────┘┴ └───────────────┘└────┘ └┘
typ └────┘ ┴ └──┘┴┴└┘ └──────────┘┴ └───────────────┘└────┘┴└┘
doc └────┘ ┴ ┴ └┘ ┴ └────┘ └┘
txt └────┘ ┴ ┴ └┘ ┴ └────┘ └┘
par └────┘ ┴ ┴ └┘ ┴ └────┘ └┘
pid ┴ ┴ ┴ └┘ ┴ └────┘ ┴┴
st ──────────────────────────────────────────────────────────────────────────┘└─┘└
170 have yball : ∀n, y ∈ closed_ball (c n) (r n),
id ┴ └─────────┘ ┴ ┴
src └───────────┘ ┴ ┴ ┴ ┴└─────────┘┴ ┴ └┘ ┴ ┴
typ └───────────┘ ┴ ┴┴┴ ┴└─────────┘┴ ┴┴ └┘ ┴┴ ┴
doc └───────────┘ ┴ ┴ ┴ ┴└─────────┘┴ ┴ └┘ ┴ ┴
txt └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
par └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
pid └────────┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
st ─────────────────────────────────────────────┘└─
171 { assume n,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───┘└──────┘└─
172 refine mem_of_closed_of_tendsto (by simp) ylim is_closed_ball _,
id └──────────────────────┘ └──┘ └────────────┘
src └─────┘└──────────────────────┘┴ ┴└──┘└┘ ┴└────────────┘└┘
typ └─────┘└──────────────────────┘┴ ┴└──┘└┘└──┘┴└────────────┘└┘
doc └─────┘ ┴ ┴└──┘└┘ ┴ └┘
txt └─────┘ ┴ ┴└──┘└┘ ┴ └┘
par └─────┘ ┴ ┴└──┘└┘ ┴ └┘
pid ┴ ┴ └─────┘ ┴ └┘
st ──────────────────────────────────────┘└───┘└─────────────────────┘└─
173 simp only [filter.mem_at_top_sets, nonempty_of_inhabited, set.mem_preimage],
id └────────────────────┘ └───────────────────┘ └──────────────┘
src └─────────┘└────────────────────┘└┘└───────────────────┘└┘└──────────────┘┴
typ └─────────┘└────────────────────┘└┘└───────────────────┘└┘└──────────────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st ──────────────────────────────────────────────────────────────────────────────┘└─
174 exact ⟨n, λm hm, I n m hm (mem_closed_ball_self (le_of_lt (rpos m)))⟩ },
id ┴ ┴ └──────────────────┘ └──────┘ └──┘
src └────┘ └┘ └────┘ ┴ ┴ ┴ ┴ └──────────────────┘┴ └──────┘┴ ┴ └───┘
typ └────┘ └┘ └────┘┴┴┴┴ ┴ ┴ └──────────────────┘┴ └──────┘┴ └──┘┴ └───┘
doc └────┘ └┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘
txt └────┘ └┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘
par └────┘ └┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘
pid ┴ └┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘┴
st ─────────────────────────────────────────────────────────────────────────┘└┘└
175 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
176 show ∀n, y ∈ f n,
id ┴ ┴
src └───┘ ┴ ┴ ┴ ┴ ┴
typ └───┘ ┴ ┴┴┴ ┴┴┴
doc └───┘ ┴ ┴ ┴ ┴ ┴
txt └───┘ ┴ ┴ ┴ ┴ ┴
par └───┘ ┴ ┴ ┴ ┴ ┴
pid └───┘ ┴ ┴ ┴ ┴ ┴
st ────────────────────
177 { assume n,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───┘└──────┘└─
178 have : closed_ball (c (n+1)) (r (n+1)) ⊆ f n := subset.trans (incl n) (inter_subset_right _ _),
id └─────────┘ ┴ ┴ ┴ ┴ └──────────┘ └──┘ ┴ └────────────────┘
src └─────┘└─────────┘┴ ┴ └──┘ ┴ └──┘ ┴ ┴ └──┘└──────────┘┴ ┴ └┘ └────────────────┘└───┘
typ └─────┘└─────────┘┴ ┴┴ └──┘ ┴┴ └──┘ ┴┴┴┴└──┘└──────────┘┴ └──┘┴┴└┘ └────────────────┘└───┘
doc └─────┘└─────────┘┴ ┴ └──┘ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ └┘ └───┘
txt └─────┘ ┴ ┴ └──┘ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ └┘ └───┘
par └─────┘ ┴ ┴ └──┘ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ └┘ └───┘
pid └───┘└┘ ┴ ┴ └──┘ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ └┘ └───┘
st ─────────────────────────────────────────────────────────────────────────────────────────────────┘└─
179 exact this (yball (n+1)) },
id └──┘ └───┘ ┴
src └────┘ ┴ ┴ └──┘
typ └────┘└──┘┴ └───┘┴ ┴ └──┘
doc └────┘ ┴ ┴ └──┘
txt └────┘ ┴ ┴ └──┘
par └────┘ ┴ ┴ └──┘
pid ┴ ┴ ┴ └─┘┴
st ────────────────────────────┘└┘└
180 show dist x y < ε, from calc
id └──┘ ┴ ┴ ┴
src └───┘└──┘┴ ┴ ┴ ┴ └───┘ └
typ └───┘└──┘┴┴┴┴┴ ┴┴ └───┘ └
doc └───┘ ┴ ┴ ┴ ┴ └───┘ └
txt └───┘ ┴ ┴ ┴ ┴ └───┘ └
par └───┘ ┴ ┴ ┴ ┴ └───┘ └
pid └───┘ ┴ ┴ ┴ ┴ └───┘ └
st ───────────────────────────────
181 dist x y = dist y x : dist_comm _ _
id └──┘ ┴ ┴ └───────┘
src ───┘ ┴ ┴ ┴ ┴└──┘┴ ┴ └─┘└───────┘└────
typ ───┘ ┴ ┴ ┴ ┴└──┘┴┴┴┴└─┘└───────┘└────
doc ───┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └────
txt ───┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └────
par ───┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └────
pid ───┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └────
st ────────────────────────────────────────
182 ... ≤ r 0 : yball 0
id ┴ └───┘
src ───────┘ ┴ └───┘ └──
typ ───────┘ ┴┴└───┘└───┘└──
doc ───────┘ ┴ └───┘ └──
txt ───────┘ ┴ └───┘ └──
par ───────┘ ┴ └───┘ └──
pid ───────┘ ┴ └───┘ └──
st ────────────────────────
183 ... < ε : lt_of_le_of_lt (min_le_left _ _) (half_lt_self εpos)
id ┴ └────────────┘ └─────────┘ └──────────┘ └──┘
src ───────┘ ┴ └─┘└────────────┘┴ └─────────┘└────┘ └──────────┘┴ └┘
typ ───────┘ ┴┴└─┘└────────────┘┴ └─────────┘└────┘ └──────────┘┴└──┘└┘
doc ───────┘ ┴ └─┘ ┴ └────┘ ┴ └┘
txt ───────┘ ┴ └─┘ ┴ └────┘ ┴ └┘
par ───────┘ ┴ └─┘ ┴ └────┘ ┴ └┘
pid ───────┘ ┴ └─┘ ┴ └────┘ ┴ ┴┴
st ──────────────────────────────────────────────────────────────────┘
184 end
st └─┘
185
186 /-- Baire theorem: a countable intersection of dense open sets is dense. Formulated here with ⋂₀. -/
187 theorem dense_sInter_of_open {S : set (set α)} (ho : ∀s∈S, is_open s) (hS : countable S)
id └─┘ └─┘ ┴ ┴ ┴ └─────┘ ┴ └───────┘ ┴
src └─┘ └─┘ └─────┘ └───────┘
typ └─┘ └─┘ ┴ ┴ ┴ └─────┘ ┴ └───────┘ ┴
doc └─────┘ └───────┘
188 (hd : ∀s∈S, closure s = univ) : closure (⋂₀S) = univ :=
id ┴ ┴ └─────┘ ┴ ┴ └──┘ └─────┘ └┘┴ ┴ └──┘
src └─────┘ ┴ └──┘ └─────┘ └┘ ┴ └──┘
typ ┴ ┴ └─────┘ ┴ ┴ └──┘ └─────┘ └┘┴ ┴ └──┘
doc └─────┘ └─────┘ └┘
189 begin
st └─────
190 cases S.eq_empty_or_nonempty with h h,
id └────────────────────┘
src └────┘└────────────────────┘└───────┘
typ └────┘└────────────────────┘└───────┘
doc └────┘ └───────┘
txt └────┘ └───────┘
par └────┘ └───────┘
pid ┴ └───────┘
st ──────────────────────────────────────┘└─
191 { simp [h] },
id ┴
src └────┘ └┘
typ └────┘┴└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ───┘└───────┘└┘└
192 { rcases exists_surjective_of_countable h hS with ⟨f, hf⟩,
id └────────────────────────────┘ ┴ └┘
src └─────┘└────────────────────────────┘┴ ┴ └───────────┘
typ └─────┘└────────────────────────────┘┴┴┴└┘└───────────┘
doc └─────┘ ┴ ┴ └───────────┘
txt └─────┘ ┴ ┴ └───────────┘
par └─────┘ ┴ ┴ └───────────┘
pid ┴ ┴ ┴ └───────────┘
st ──────────────────────────────────────────────────────────┘└─
193 have F : ∀n, f n ∈ S := λn, by rw hf; exact mem_range_self _,
id ┴ ┴ ┴ └┘ └────────────┘
src └───────┘ ┴ ┴ ┴ ┴┴┴ └──┘ └─┘ ┴└─┘ └┘└────┘└────────────┘└┘
typ └───────┘ ┴ ┴┴┴ ┴┴┴┴└──┘ └─┘ ┴└─┘└┘└┘└────┘└────────────┘└┘
doc └───────┘ ┴ ┴ ┴ ┴ ┴ └──┘ └─┘ ┴└─┘ └┘└────┘ └┘
txt └───────┘ ┴ ┴ ┴ ┴ ┴ └──┘ └─┘ ┴└─┘ └┘└────┘ └┘
par └───────┘ ┴ ┴ ┴ ┴ ┴ └──┘ └─┘ ┴└─┘ └┘└────┘ └┘
pid └────┘└─┘ ┴ ┴ ┴ ┴ ┴ └──┘ └─┘ └──┘ └──────┘ └┘
st ─────────────────────────────────┘└────────────────────────────┘└─
194 rw [hf, sInter_range],
id └┘ └──────────┘
src └──┘ └┘└──────────┘┴
typ └──┘└┘└┘└──────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ─────────┘└────────────┘└──
195 exact dense_Inter_of_open_nat (λn, ho _ (F n)) (λn, hd _ (F n)) }
id └─────────────────────┘ └┘ └┘ ┴
src └────┘└─────────────────────┘┴ └─┘ └─┘ ┴ └─┘ └─┘ └─┘ ┴ └─┘
typ └────┘└─────────────────────┘┴ └─┘└┘└─┘ ┴ └─┘ └─┘└┘└─┘ ┴┴ └─┘
doc └────┘└─────────────────────┘┴ └─┘ └─┘ ┴ └─┘ └─┘ └─┘ ┴ └─┘
txt └────┘ ┴ └─┘ └─┘ ┴ └─┘ └─┘ └─┘ ┴ └─┘
par └────┘ ┴ └─┘ └─┘ ┴ └─┘ └─┘ └─┘ ┴ └─┘
pid ┴ ┴ └─┘ └─┘ ┴ └─┘ └─┘ └─┘ ┴ └┘┴
st ───────────────────────────────────────────────────────────────────┘└─
196 end
st ──┘
197
198 /-- Baire theorem: a countable intersection of dense open sets is dense. Formulated here with
199 an index set which is a countable set in any type. -/
200 theorem dense_bInter_of_open {S : set β} {f : β → set α} (ho : ∀s∈S, is_open (f s))
id └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ └─────┘ ┴ ┴
src └─┘ └─┘ └─────┘
typ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ └─────┘ ┴ ┴
doc └─────┘
201 (hS : countable S) (hd : ∀s∈S, closure (f s) = univ) : closure (⋂s∈S, f s) = univ :=
id └───────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └──┘ └─────┘ ┴┴ ┴┴ ┴ ┴ ┴ └──┘
src └───────┘ └─────┘ ┴ └──┘ └─────┘ ┴ ┴ ┴ └──┘
typ └───────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └──┘ └─────┘ ┴┴ ┴┴ ┴ ┴ ┴ └──┘
doc └───────┘ └─────┘ └─────┘ ┴ ┴
202 begin
st └─────
203 rw ← sInter_image,
id └──────────┘
src └───┘└──────────┘
typ └───┘└──────────┘
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ──────────────────┘└─
204 apply dense_sInter_of_open,
id └──────────────────┘
src └────┘└──────────────────┘
typ └────┘└──────────────────┘
doc └────┘└──────────────────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────────────┘└─
205 { rwa ball_image_iff },
id └────────────┘
src └──┘└────────────┘┴
typ └──┘└────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid ┴ ┴
st ───┘└─────────────────┘└┘└
206 { exact countable_image _ hS },
id └─────────────┘ └┘
src └────┘└─────────────┘└─┘ ┴
typ └────┘└─────────────┘└─┘└┘┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ───┘└─────────────────────────┘└┘└
207 { rwa ball_image_iff }
id └────────────┘
src └──┘└────────────┘┴
typ └──┘└────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid ┴ ┴
st ──────────────────────┘└─
208 end
st ──┘
209
210 /-- Baire theorem: a countable intersection of dense open sets is dense. Formulated here with
211 an index set which is an encodable type. -/
212 theorem dense_Inter_of_open [encodable β] {f : β → set α} (ho : ∀s, is_open (f s))
id └───────┘ ┴ ┴ └─┘ ┴ ┴ └─────┘ ┴ ┴
src └───────┘ └─┘ └─────┘
typ └───────┘ ┴ ┴ └─┘ ┴ ┴ └─────┘ ┴ ┴
doc └───────┘ └─────┘
213 (hd : ∀s, closure (f s) = univ) : closure (⋂s, f s) = univ :=
id ┴ └─────┘ ┴ ┴ ┴ └──┘ └─────┘ ┴┴┴ ┴ ┴ ┴ └──┘
src └─────┘ ┴ └──┘ └─────┘ ┴ ┴ ┴ └──┘
typ ┴ └─────┘ ┴ ┴ ┴ └──┘ └─────┘ ┴┴┴ ┴ ┴ ┴ └──┘
doc └─────┘ └─────┘ ┴ ┴
214 begin
st └─────
215 rw ← sInter_range,
id └──────────┘
src └───┘└──────────┘
typ └───┘└──────────┘
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ──────────────────┘└─
216 apply dense_sInter_of_open,
id └──────────────────┘
src └────┘└──────────────────┘
typ └────┘└──────────────────┘
doc └────┘└──────────────────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────────────┘└─
217 { rwa forall_range_iff },
id └──────────────┘
src └──┘└──────────────┘┴
typ └──┘└──────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid ┴ ┴
st ───┘└───────────────────┘└┘└
218 { exact countable_range _ },
id └─────────────┘
src └────┘└─────────────┘└─┘
typ └────┘└─────────────┘└─┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └┘┴
st ───┘└──────────────────────┘└┘└
219 { rwa forall_range_iff }
id └──────────────┘
src └──┘└──────────────┘┴
typ └──┘└──────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid ┴ ┴
st ────────────────────────┘└─
220 end
st ──┘
221
222 /-- Baire theorem: a countable intersection of dense Gδ sets is dense. Formulated here with ⋂₀. -/
223 theorem dense_sInter_of_Gδ {S : set (set α)} (ho : ∀s∈S, is_Gδ s) (hS : countable S)
id └─┘ └─┘ ┴ ┴ ┴ └───┘ ┴ └───────┘ ┴
src └─┘ └─┘ └───┘ └───────┘
typ └─┘ └─┘ ┴ ┴ ┴ └───┘ ┴ └───────┘ ┴
doc └───┘ └───────┘
224 (hd : ∀s∈S, closure s = univ) : closure (⋂₀S) = univ :=
id ┴ ┴ └─────┘ ┴ ┴ └──┘ └─────┘ └┘┴ ┴ └──┘
src └─────┘ ┴ └──┘ └─────┘ └┘ ┴ └──┘
typ ┴ ┴ └─────┘ ┴ ┴ └──┘ └─────┘ └┘┴ ┴ └──┘
doc └─────┘ └─────┘ └┘
225 begin
st └─────
226 -- the result follows from the result for a countable intersection of dense open sets,
st ─────────────────────────────────────────────────────────────────────────────────────────
227 -- by rewriting each set as a countable intersection of open sets, which are of course dense.
st ────────────────────────────────────────────────────────────────────────────────────────────────
228 have : ∀s : set α, ∃T : set (set α), s ∈ S → ((∀t ∈ T, is_open t) ∧ countable T ∧ s = (⋂₀ T)),
id └─┘ ┴ └─┘ └─┘ ┴ ┴ ┴ ┴ └─────┘ ┴ └───────┘ ┴ └┘
src └─────┘ └──┘ ┴ ┴┴└──┘ ┴ └─┘┴ ┴┴┴ ┴ ┴ ┴ ┴ └──┘ ┴└─────┘┴ └┘┴┴└───────┘┴ ┴ ┴ ┴┴┴ └┘┴ └┘
typ └─────┘ └──┘└─┘┴ ┴┴└──┘└─┘┴ └─┘┴┴┴┴┴ ┴┴┴┴┴ ┴ └──┘ ┴└─────┘┴ └┘┴┴└───────┘┴ ┴ ┴ ┴┴┴ └┘┴ └┘
doc └─────┘ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴└─────┘┴ └┘ ┴└───────┘┴ ┴ ┴ ┴ ┴ └┘┴ └┘
txt └─────┘ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
par └─────┘ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
pid └───┘└┘ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
st ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
229 { assume s,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───┘└──────┘└─
230 by_cases hs : s ∈ S,
id ┴ ┴
src └───────┘ └─┘ ┴ ┴
typ └───────┘ └─┘┴┴ ┴┴
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ──────────────────────┘└─
231 { simp [hs], exact ho s hs },
id └┘ └┘ ┴ └┘
src └────┘ ┴ └────┘ ┴ ┴ ┴
typ └────┘└┘┴ └────┘└┘┴┴┴└┘┴
doc └────┘ ┴ └────┘ ┴ ┴ ┴
txt └────┘ ┴ └────┘ ┴ ┴ ┴
par └────┘ ┴ └────┘ ┴ ┴ ┴
pid ┴┴ ┴ ┴ ┴ ┴ ┴
st ─────┘└───────┘└──────────────┘└┘└
232 { simp [hs] }},
id └┘
src └────┘ └┘
typ └────┘└┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ───────────────┘└─┘└
233 choose T hT using this,
id └──┘
src └────────────────┘
typ └────────────────┘└──┘
doc └────────────────┘
txt └────────────────┘
par └────────────────┘
pid └┘└─┘└─────┘
st ───────────────────────┘└─
234 have : ⋂₀ S = ⋂₀ (⋃s∈S, T s) := (sInter_bUnion (λs hs, (hT s hs).2.2)).symm,
id ┴ ┴┴ ┴ └───────────┘ └┘
src └─────┘ ┴ ┴ ┴ ┴ ┴└┘ ┴┴ ┴ └───┘ └───────────┘┴ └────┘ ┴ ┴ └──────────┘
typ └─────┘ ┴ ┴ ┴ ┴ ┴└┘┴┴┴┴┴ └───┘ └───────────┘┴ └────┘ └┘┴ ┴ └──────────┘
doc └─────┘ ┴ ┴ ┴ ┴ ┴└┘ ┴┴ ┴ └───┘ ┴ └────┘ ┴ ┴ └──────────┘
txt └─────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └───┘ ┴ └────┘ ┴ ┴ └──────────┘
par └─────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └───┘ ┴ └────┘ ┴ ┴ └──────────┘
pid └───┘└┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴└──┘ ┴ └────┘ ┴ ┴ └─────────┘┴
st ────────────────────────────────────────────────────────────────────────────┘└─
235 rw this,
id └──┘
src └─┘
typ └─┘└──┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────┘└─
236 refine dense_sInter_of_open (λt ht, _) (countable_bUnion hS (λs hs, (hT s hs).2.1)) (λt ht, _),
id └──────────────────┘ └──────────────┘ └┘ └┘
src └─────┘└──────────────────┘┴ └───────┘ └──────────────┘┴ ┴ └────┘ ┴ ┴ └──────┘ └──────┘
typ └─────┘└──────────────────┘┴ └───────┘ └──────────────┘┴└┘┴ └────┘ └┘┴ ┴ └──────┘ └──────┘
doc └─────┘└──────────────────┘┴ └───────┘ ┴ ┴ └────┘ ┴ ┴ └──────┘ └──────┘
txt └─────┘ ┴ └───────┘ ┴ ┴ └────┘ ┴ ┴ └──────┘ └──────┘
par └─────┘ ┴ └───────┘ ┴ ┴ └────┘ ┴ ┴ └──────┘ └──────┘
pid ┴ ┴ └───────┘ ┴ ┴ └────┘ ┴ ┴ └──────┘ └──────┘
st ───────────────────────────────────────────────────────────────────────────────────────────────┘└─
237 show is_open t,
id └─────┘ ┴
src └───┘└─────┘┴
typ └───┘└─────┘┴┴
doc └───┘└─────┘┴
txt └───┘ ┴
par └───┘ ┴
pid └───┘ ┴
st ──────────────────
238 { simp only [exists_prop, set.mem_Union] at ht,
id └─────────┘ └───────────┘
src └─────────┘└─────────┘└┘└───────────┘└─────┘
typ └─────────┘└─────────┘└┘└───────────┘└─────┘
doc └─────────┘ └┘ └─────┘
txt └─────────┘ └┘ └─────┘
par └─────────┘ └┘ └─────┘
pid ┴└──┘└┘ └┘ ┴┴└───┘
st ───┘└──────────────────────────────────────────┘└─
239 rcases ht with ⟨s, hs, tTs⟩,
id └┘
src └─────┘ └────────────────┘
typ └─────┘└┘└────────────────┘
doc └─────┘ └────────────────┘
txt └─────┘ └────────────────┘
par └─────┘ └────────────────┘
pid ┴ └────────────────┘
st ──────────────────────────────┘└─
240 exact (hT s hs).1 t tTs },
id └┘ ┴ └┘ ┴ └─┘
src └────┘ ┴ ┴ └──┘ ┴ ┴
typ └────┘ └┘┴┴┴└┘└──┘┴┴└─┘┴
doc └────┘ ┴ ┴ └──┘ ┴ ┴
txt └────┘ ┴ ┴ └──┘ ┴ ┴
par └────┘ ┴ ┴ └──┘ ┴ ┴
pid ┴ ┴ ┴ └──┘ ┴ ┴
st ───────────────────────────┘└┘└
241 show closure t = univ,
id └─────┘ ┴ └──┘
src └───┘└─────┘┴ ┴ ┴└──┘
typ └───┘└─────┘┴┴┴ ┴└──┘
doc └───┘└─────┘┴ ┴ ┴
txt └───┘ ┴ ┴ ┴
par └───┘ ┴ ┴ ┴
pid └───┘ ┴ ┴ ┴
st ─────────────────────────
242 { simp only [exists_prop, set.mem_Union] at ht,
id └─────────┘ └───────────┘
src └─────────┘└─────────┘└┘└───────────┘└─────┘
typ └─────────┘└─────────┘└┘└───────────┘└─────┘
doc └─────────┘ └┘ └─────┘
txt └─────────┘ └┘ └─────┘
par └─────────┘ └┘ └─────┘
pid ┴└──┘└┘ └┘ ┴┴└───┘
st ───────────────────────────────────────────────┘└─
243 rcases ht with ⟨s, hs, tTs⟩,
id └┘
src └─────┘ └────────────────┘
typ └─────┘└┘└────────────────┘
doc └─────┘ └────────────────┘
txt └─────┘ └────────────────┘
par └─────┘ └────────────────┘
pid ┴ └────────────────┘
st ──────────────────────────────┘└─
244 apply subset.antisymm (subset_univ _),
id └─────────────┘ └─────────┘
src └────┘└─────────────┘┴ └─────────┘└─┘
typ └────┘└─────────────┘┴ └─────────┘└─┘
doc └────┘ ┴ └─┘
txt └────┘ ┴ └─┘
par └────┘ ┴ └─┘
pid ┴ ┴ └─┘
st ────────────────────────────────────────┘└─
245 rw ← (hd s hs),
id └┘ ┴ └┘
src └───┘ ┴ ┴ ┴
typ └───┘ └┘┴┴┴└┘┴
doc └───┘ ┴ ┴ ┴
txt └───┘ ┴ ┴ ┴
par └───┘ ┴ ┴ ┴
pid └─┘ ┴ ┴ ┴
st ─────────────────┘└─
246 apply closure_mono,
id └──────────┘
src └────┘└──────────┘
typ └────┘└──────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────┘└─
247 have := sInter_subset_of_mem tTs,
id └──────────────────┘ └─┘
src └──────┘└──────────────────┘┴
typ └──────┘└──────────────────┘┴└─┘
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid └───┘└─┘ ┴
st ───────────────────────────────────┘└─
248 rwa ← (hT s hs).2.2 at this }
id └┘ ┴ └┘
src └────┘ ┴ ┴ └────────────┘
typ └────┘ └┘┴┴┴└┘└────────────┘
doc └────┘ ┴ ┴ └────────────┘
txt └────┘ ┴ ┴ └────────────┘
par └────┘ ┴ ┴ └────────────┘
pid └─┘ ┴ ┴ └─┘└────────┘┴
st ───────────────────────────────┘└─
249 end
st ──┘
250
251 /-- Baire theorem: a countable intersection of dense Gδ sets is dense. Formulated here with
252 an index set which is a countable set in any type. -/
253 theorem dense_bInter_of_Gδ {S : set β} {f : β → set α} (ho : ∀s∈S, is_Gδ (f s))
id └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ └───┘ ┴ ┴
src └─┘ └─┘ └───┘
typ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ └───┘ ┴ ┴
doc └───┘
254 (hS : countable S) (hd : ∀s∈S, closure (f s) = univ) : closure (⋂s∈S, f s) = univ :=
id └───────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └──┘ └─────┘ ┴┴ ┴┴ ┴ ┴ ┴ └──┘
src └───────┘ └─────┘ ┴ └──┘ └─────┘ ┴ ┴ ┴ └──┘
typ └───────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └──┘ └─────┘ ┴┴ ┴┴ ┴ ┴ ┴ └──┘
doc └───────┘ └─────┘ └─────┘ ┴ ┴
255 begin
st └─────
256 rw ← sInter_image,
id └──────────┘
src └───┘└──────────┘
typ └───┘└──────────┘
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ──────────────────┘└─
257 apply dense_sInter_of_Gδ,
id └────────────────┘
src └────┘└────────────────┘
typ └────┘└────────────────┘
doc └────┘└────────────────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────┘└─
258 { rwa ball_image_iff },
id └────────────┘
src └──┘└────────────┘┴
typ └──┘└────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid ┴ ┴
st ───┘└─────────────────┘└┘└
259 { exact countable_image _ hS },
id └─────────────┘ └┘
src └────┘└─────────────┘└─┘ ┴
typ └────┘└─────────────┘└─┘└┘┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ───┘└─────────────────────────┘└┘└
260 { rwa ball_image_iff }
id └────────────┘
src └──┘└────────────┘┴
typ └──┘└────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid ┴ ┴
st ──────────────────────┘└─
261 end
st ──┘
262
263 /-- Baire theorem: a countable intersection of dense Gδ sets is dense. Formulated here with
264 an index set which is an encodable type. -/
265 theorem dense_Inter_of_Gδ [encodable β] {f : β → set α} (ho : ∀s, is_Gδ (f s))
id └───────┘ ┴ ┴ └─┘ ┴ ┴ └───┘ ┴ ┴
src └───────┘ └─┘ └───┘
typ └───────┘ ┴ ┴ └─┘ ┴ ┴ └───┘ ┴ ┴
doc └───────┘ └───┘
266 (hd : ∀s, closure (f s) = univ) : closure (⋂s, f s) = univ :=
id ┴ └─────┘ ┴ ┴ ┴ └──┘ └─────┘ ┴┴┴ ┴ ┴ ┴ └──┘
src └─────┘ ┴ └──┘ └─────┘ ┴ ┴ ┴ └──┘
typ ┴ └─────┘ ┴ ┴ ┴ └──┘ └─────┘ ┴┴┴ ┴ ┴ ┴ └──┘
doc └─────┘ └─────┘ ┴ ┴
267 begin
st └─────
268 rw ← sInter_range,
id └──────────┘
src └───┘└──────────┘
typ └───┘└──────────┘
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ──────────────────┘└─
269 apply dense_sInter_of_Gδ,
id └────────────────┘
src └────┘└────────────────┘
typ └────┘└────────────────┘
doc └────┘└────────────────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────┘└─
270 { rwa forall_range_iff },
id └──────────────┘
src └──┘└──────────────┘┴
typ └──┘└──────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid ┴ ┴
st ───┘└───────────────────┘└┘└
271 { exact countable_range _ },
id └─────────────┘
src └────┘└─────────────┘└─┘
typ └────┘└─────────────┘└─┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └┘┴
st ───┘└──────────────────────┘└┘└
272 { rwa forall_range_iff }
id └──────────────┘
src └──┘└──────────────┘┴
typ └──┘└──────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid ┴ ┴
st ────────────────────────┘└─
273 end
st ──┘
274
275 /-- Baire theorem: if countably many closed sets cover the whole space, then their interiors
276 are dense. Formulated here with an index set which is a countable set in any type. -/
277 theorem dense_bUnion_interior_of_closed {S : set β} {f : β → set α} (hc : ∀s∈S, is_closed (f s))
id └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ └───────┘ ┴ ┴
src └─┘ └─┘ └───────┘
typ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ └───────┘ ┴ ┴
doc └───────┘
278 (hS : countable S) (hU : (⋃s∈S, f s) = univ) : closure (⋃s∈S, interior (f s)) = univ :=
id └───────┘ ┴ ┴┴ ┴┴ ┴ ┴ ┴ └──┘ └─────┘ ┴┴ ┴┴ └──────┘ ┴ ┴ ┴ └──┘
src └───────┘ ┴ ┴ ┴ └──┘ └─────┘ ┴ ┴ └──────┘ ┴ └──┘
typ └───────┘ ┴ ┴┴ ┴┴ ┴ ┴ ┴ └──┘ └─────┘ ┴┴ ┴┴ └──────┘ ┴ ┴ ┴ └──┘
doc └───────┘ ┴ ┴ └─────┘ ┴ ┴ └──────┘
279 begin
st └─────
280 let g := λs, - (frontier (f s)),
id ┴ └──────┘ ┴
src └───────┘ └─┘┴┴ └──────┘┴ ┴ └┘
typ └───────┘ └─┘┴┴ └──────┘┴ ┴┴ └┘
doc └───────┘ └─┘ ┴ └──────┘┴ ┴ └┘
txt └───────┘ └─┘ ┴ ┴ ┴ └┘
par └───────┘ └─┘ ┴ ┴ ┴ └┘
pid └───┘┴└─┘ └─┘ ┴ ┴ ┴ └┘
st ────────────────────────────────┘└─
281 have clos_g : closure (⋂s∈S, g s) = univ,
id └─────┘ ┴ ┴┴ ┴ ┴ └──┘
src └────────────┘└─────┘┴ ┴└┘ ┴┴ ┴ └┘┴┴└──┘
typ └────────────┘└─────┘┴ ┴└┘┴┴┴┴┴ └┘┴┴└──┘
doc └────────────┘└─────┘┴ ┴└┘ ┴┴ ┴ └┘ ┴
txt └────────────┘ ┴ └┘ ┴ ┴ └┘ ┴
par └────────────┘ ┴ └┘ ┴ ┴ └┘ ┴
pid └─────────┘└─┘ ┴ └┘ ┴ ┴ └┘ ┴
st ─────────────────────────────────────────┘└─
282 { refine dense_bInter_of_open (λs hs, _) hS (λs hs, _),
id └──────────────────┘ └┘
src └─────┘└──────────────────┘┴ └───────┘ ┴ └──────┘
typ └─────┘└──────────────────┘┴ └───────┘└┘┴ └──────┘
doc └─────┘└──────────────────┘┴ └───────┘ ┴ └──────┘
txt └─────┘ ┴ └───────┘ ┴ └──────┘
par └─────┘ ┴ └───────┘ ┴ └──────┘
pid ┴ ┴ └───────┘ ┴ └──────┘
st ───┘└──────────────────────────────────────────────────┘└─
283 show is_open (g s), from is_open_compl_iff.2 is_closed_frontier,
id └─────┘ ┴ ┴ └───────────────┘ └────────────────┘
src └───┘└─────┘┴ ┴ ┴ └───┘└───────────────┘└─┘└────────────────┘
typ └───┘└─────┘┴ ┴┴┴┴ └───┘└───────────────┘└─┘└────────────────┘
doc └───┘└─────┘┴ ┴ ┴ └───┘ └─┘└────────────────┘
txt └───┘ ┴ ┴ ┴ └───┘ └─┘
par └───┘ ┴ ┴ ┴ └───┘ └─┘
pid └───┘ ┴ ┴ ┴ └───┘ └─┘
st ──────────────────────────────────────────────────────────────────┘└─
284 show closure (g s) = univ,
id └─────┘ ┴ ┴ └──┘
src └───┘└─────┘┴ ┴ └┘ ┴└──┘
typ └───┘└─────┘┴ ┴┴┴└┘ ┴└──┘
doc └───┘└─────┘┴ ┴ └┘ ┴
txt └───┘ ┴ ┴ └┘ ┴
par └───┘ ┴ ┴ └┘ ┴
pid └───┘ ┴ ┴ └┘ ┴
st ───────────────────────────────
285 { apply subset.antisymm (subset_univ _),
id └─────────────┘ └─────────┘
src └────┘└─────────────┘┴ └─────────┘└─┘
typ └────┘└─────────────┘┴ └─────────┘└─┘
doc └────┘ ┴ └─┘
txt └────┘ ┴ └─┘
par └────┘ ┴ └─┘
pid ┴ ┴ └─┘
st ──────────────────────────────────────────┘└─
286 simp [g, interior_frontier (hc s hs)] }},
id ┴ └───────────────┘ └┘ ┴ └┘
src └────┘ └┘└───────────────┘┴ ┴ ┴ └─┘
typ └────┘┴└┘└───────────────┘┴ └┘┴┴┴└┘└─┘
doc └────┘ └┘└───────────────┘┴ ┴ ┴ └─┘
txt └────┘ └┘ ┴ ┴ ┴ └─┘
par └────┘ └┘ ┴ ┴ ┴ └─┘
pid ┴┴ └┘ ┴ ┴ ┴ └┘┴
st ──────────────────────────────────────────┘└─┘└
287 have : (⋂s∈S, g s) ⊆ (⋃s∈S, interior (f s)),
id ┴ ┴ ┴ ┴ ┴ ┴┴ └──────┘ ┴
src └─────┘ ┴└┘ ┴┴ ┴ └┘┴┴ ┴└┘ ┴┴└──────┘┴ ┴ └┘
typ └─────┘ ┴└┘ ┴┴┴┴ └┘┴┴ ┴└┘┴┴┴└──────┘┴ ┴┴ └┘
doc └─────┘ ┴└┘ ┴┴ ┴ └┘ ┴ ┴└┘ ┴┴└──────┘┴ ┴ └┘
txt └─────┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘
par └─────┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘
pid └───┘└┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘
st ────────────────────────────────────────────┘└─
288 { assume x hx,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ───┘└─────────┘└─
289 have : x ∈ ⋃s∈S, f s, { have := mem_univ x, rwa ← hU at this },
id ┴ ┴ ┴┴ ┴ └──────┘ ┴ └┘
src └─────┘ ┴ ┴┴└┘ ┴┴ ┴ └──────┘└──────┘┴ └────┘ └───────┘
typ └─────┘┴┴ ┴┴└┘┴┴┴┴┴ └──────┘└──────┘┴┴ └────┘└┘└───────┘
doc └─────┘ ┴ ┴┴└┘ ┴┴ ┴ └──────┘ ┴ └────┘ └───────┘
txt └─────┘ ┴ ┴ └┘ ┴ ┴ └──────┘ ┴ └────┘ └───────┘
par └─────┘ ┴ ┴ └┘ ┴ ┴ └──────┘ ┴ └────┘ └───────┘
pid └───┘└┘ ┴ ┴ └┘ ┴ ┴ └───┘└─┘ ┴ └─┘ └──────┘┴
st ───────────────────────┘└──┘└────────────────┘└─────────────────┘└┘└
290 rcases mem_bUnion_iff.1 this with ⟨s, hs, xs⟩,
id └────────────┘ └──┘
src └─────┘└────────────┘└─┘ └───────────────┘
typ └─────┘└────────────┘└─┘└──┘└───────────────┘
doc └─────┘ └─┘ └───────────────┘
txt └─────┘ └─┘ └───────────────┘
par └─────┘ └─┘ └───────────────┘
pid ┴ └─┘ └───────────────┘
st ────────────────────────────────────────────────┘└─
291 have : x ∈ g s := mem_bInter_iff.1 hx s hs,
id ┴ ┴ ┴ └────────────┘ └┘ ┴ └┘
src └─────┘ ┴ ┴ ┴ └──┘└────────────┘└─┘ ┴ ┴
typ └─────┘┴┴ ┴┴┴┴└──┘└────────────┘└─┘└┘┴┴┴└┘
doc └─────┘ ┴ ┴ ┴ └──┘ └─┘ ┴ ┴
txt └─────┘ ┴ ┴ ┴ └──┘ └─┘ ┴ ┴
par └─────┘ ┴ ┴ ┴ └──┘ └─┘ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴ └──┘ └─┘ ┴ ┴
st ─────────────────────────────────────────────┘└─
292 have : x ∈ interior (f s),
id ┴ └──────┘ ┴ ┴
src └─────┘ ┴ ┴└──────┘┴ ┴ ┴
typ └─────┘┴┴ ┴└──────┘┴ ┴┴┴┴
doc └─────┘ ┴ ┴└──────┘┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────┘└─
293 { have : x ∈ f s \ (frontier (f s)) := mem_inter xs this,
id ┴ ┴ └──────┘ ┴ ┴ └───────┘ └┘ └──┘
src └─────┘ ┴ ┴ ┴ ┴┴┴ └──────┘┴ ┴ └────┘└───────┘┴ ┴
typ └─────┘┴┴ ┴ ┴ ┴┴┴ └──────┘┴ ┴┴┴└────┘└───────┘┴└┘┴└──┘
doc └─────┘ ┴ ┴ ┴ ┴ ┴ └──────┘┴ ┴ └────┘ ┴ ┴
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘└──┘ ┴ ┴
st ─────┘└────────────────────────────────────────────────────┘└─
294 simpa [frontier, xs, closure_eq_of_is_closed (hc s hs)] using this },
id └──────┘ └┘ └─────────────────────┘ └┘ ┴ └┘ └──┘
src └─────┘└──────┘└┘ └┘└─────────────────────┘┴ ┴ ┴ └───────┘ ┴
typ └─────┘└──────┘└┘└┘└┘└─────────────────────┘┴ └┘┴┴┴└┘└───────┘└──┘┴
doc └─────┘└──────┘└┘ └┘ ┴ ┴ ┴ └───────┘ ┴
txt └─────┘ └┘ └┘ ┴ ┴ ┴ └───────┘ ┴
par └─────┘ └┘ └┘ ┴ ┴ ┴ └───────┘ ┴
pid ┴┴ └┘ └┘ ┴ ┴ ┴ └┘┴└────┘ ┴
st ────────────────────────────────────────────────────────────────────────┘└┘└
295 exact mem_bUnion_iff.2 ⟨s, ⟨hs, this⟩⟩ },
id └────────────┘ ┴ └┘ └──┘
src └────┘└────────────┘└─┘ └┘ └┘ └─┘
typ └────┘└────────────┘└─┘ ┴└┘ └┘└┘└──┘└─┘
doc └────┘ └─┘ └┘ └┘ └─┘
txt └────┘ └─┘ └┘ └┘ └─┘
par └────┘ └─┘ └┘ └┘ └─┘
pid ┴ └─┘ └┘ └┘ └┘┴
st ──────────────────────────────────────────┘└┘└
296 have := closure_mono this,
id └──────────┘ └──┘
src └──────┘└──────────┘┴
typ └──────┘└──────────┘┴└──┘
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid └───┘└─┘ ┴
st ──────────────────────────┘└─
297 rw clos_g at this,
id └────┘
src └─┘ └──────┘
typ └─┘└────┘└──────┘
doc └─┘ └──────┘
txt └─┘ └──────┘
par └─┘ └──────┘
pid ┴ └──────┘
st ──────────────────┘└─
298 exact subset.antisymm (subset_univ _) this
id └─────────────┘ └─────────┘ └──┘
src └────┘└─────────────┘┴ └─────────┘└──┘ ┴
typ └────┘└─────────────┘┴ └─────────┘└──┘└──┘┴
doc └────┘ ┴ └──┘ ┴
txt └────┘ ┴ └──┘ ┴
par └────┘ ┴ └──┘ ┴
pid ┴ ┴ └──┘ ┴
st ────────────────────────────────────────────┘
299 end
st └─┘
300
301 /-- Baire theorem: if countably many closed sets cover the whole space, then their interiors
302 are dense. Formulated here with ⋃₀. -/
303 theorem dense_sUnion_interior_of_closed {S : set (set α)} (hc : ∀s∈S, is_closed s)
id └─┘ └─┘ ┴ ┴ ┴ └───────┘ ┴
src └─┘ └─┘ └───────┘
typ └─┘ └─┘ ┴ ┴ ┴ └───────┘ ┴
doc └───────┘
304 (hS : countable S) (hU : (⋃₀ S) = univ) : closure (⋃s∈S, interior s) = univ :=
id └───────┘ ┴ └┘ ┴ ┴ └──┘ └─────┘ ┴┴ ┴┴ └──────┘ ┴ ┴ └──┘
src └───────┘ └┘ ┴ └──┘ └─────┘ ┴ ┴ └──────┘ ┴ └──┘
typ └───────┘ ┴ └┘ ┴ ┴ └──┘ └─────┘ ┴┴ ┴┴ └──────┘ ┴ ┴ └──┘
doc └───────┘ └─────┘ ┴ ┴ └──────┘
305 by rw sUnion_eq_bUnion at hU; exact dense_bUnion_interior_of_closed hc hS hU
id └──────────────┘ └─────────────────────────────┘ └┘ └┘ └┘
src └─┘└──────────────┘└────┘ └────┘└─────────────────────────────┘┴ ┴ ┴ └
typ └─┘└──────────────┘└────┘ └────┘└─────────────────────────────┘┴└┘┴└┘┴└┘└
doc └─┘ └────┘ └────┘└─────────────────────────────┘┴ ┴ ┴ └
txt └─┘ └────┘ └────┘ ┴ ┴ ┴ └
par └─┘ └────┘ └────┘ ┴ ┴ ┴ └
pid ┴ └────┘ ┴ ┴ ┴ ┴ └
st └──────────────────────────────────────────────────────────────────────────
306
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
307 /-- Baire theorem: if countably many closed sets cover the whole space, then their interiors
308 are dense. Formulated here with an index set which is an encodable type. -/
309 theorem dense_Union_interior_of_closed [encodable β] {f : β → set α} (hc : ∀s, is_closed (f s))
id └───────┘ ┴ ┴ └─┘ ┴ ┴ └───────┘ ┴ ┴
src └───────┘ └─┘ └───────┘
typ └───────┘ ┴ ┴ └─┘ ┴ ┴ └───────┘ ┴ ┴
doc └───────┘ └───────┘
310 (hU : (⋃s, f s) = univ) : closure (⋃s, interior (f s)) = univ :=
id ┴┴┴ ┴ ┴ ┴ └──┘ └─────┘ ┴┴┴ └──────┘ ┴ ┴ ┴ └──┘
src ┴ ┴ ┴ └──┘ └─────┘ ┴ ┴ └──────┘ ┴ └──┘
typ ┴┴┴ ┴ ┴ ┴ └──┘ └─────┘ ┴┴┴ └──────┘ ┴ ┴ ┴ └──┘
doc ┴ ┴ └─────┘ ┴ ┴ └──────┘
311 begin
st └─────
312 rw ← bUnion_univ,
id └─────────┘
src └───┘└─────────┘
typ └───┘└─────────┘
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ─────────────────┘└─
313 apply dense_bUnion_interior_of_closed,
id └─────────────────────────────┘
src └────┘└─────────────────────────────┘
typ └────┘└─────────────────────────────┘
doc └────┘└─────────────────────────────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────────────────────┘└─
314 { simp [hc] },
id └┘
src └────┘ └┘
typ └────┘└┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ───┘└────────┘└┘└
315 { apply countable_encodable },
id └─────────────────┘
src └────┘└─────────────────┘┴
typ └────┘└─────────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───┘└────────────────────────┘└┘└
316 { rwa ← bUnion_univ at hU }
id └─────────┘
src └────┘└─────────┘└─────┘
typ └────┘└─────────┘└─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid └─┘ └────┘┴
st ───────────────────────────┘└─
317 end
st ──┘
318
319 /-- One of the most useful consequences of Baire theorem: if a countable union of closed sets
320 covers the space, then one of the sets has nonempty interior. -/
321 theorem nonempty_interior_of_Union_of_closed [nonempty α] [encodable β] {f : β → set α}
id └──────┘ ┴ └───────┘ ┴ ┴ └─┘ ┴
src └──────┘ └───────┘ └─┘
typ └──────┘ ┴ └───────┘ ┴ ┴ └─┘ ┴
doc └───────┘
322 (hc : ∀s, is_closed (f s)) (hU : (⋃s, f s) = univ) : ∃s x ε, ε > 0 ∧ ball x ε ⊆ f s :=
id ┴ └───────┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ └──┘ ┴┴ ┴ ┴┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴
typ ┴ └───────┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ └──┘ ┴┴ ┴ ┴┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
doc └───────┘ ┴ ┴ └──┘
323 begin
st └─────
324 have : ∃s, (interior (f s)).nonempty,
id ┴ ┴ └──────┘ ┴
src └─────┘┴┴┴┴ └──────┘┴ ┴ └─────────┘
typ └─────┘┴┴┴┴ └──────┘┴ ┴┴ └─────────┘
doc └─────┘ ┴ ┴ └──────┘┴ ┴ └─────────┘
txt └─────┘ ┴ ┴ ┴ ┴ └─────────┘
par └─────┘ ┴ ┴ ┴ ┴ └─────────┘
pid └───┘└┘ ┴ ┴ ┴ ┴ └────────┘┴
st ─────────────────────────────────────┘└─
325 { by_contradiction h,
src └────────────────┘
typ └────────────────┘
doc └────────────────┘
txt └────────────────┘
par └────────────────┘
pid └┘
st ───┘└────────────────┘└─
326 simp only [not_exists, not_nonempty_iff_eq_empty] at h,
id └────────┘ └───────────────────────┘
src └─────────┘└────────┘└┘└───────────────────────┘└────┘
typ └─────────┘└────────┘└┘└───────────────────────┘└────┘
doc └─────────┘ └┘ └────┘
txt └─────────┘ └┘ └────┘
par └─────────┘ └┘ └────┘
pid ┴└──┘└┘ └┘ ┴┴└──┘
st ─────────────────────────────────────────────────────────┘└─
327 have := calc ∅ = closure (⋃s, interior (f s)) : by simp [h]
id ┴ └─────┘ ┴ ┴ └──────┘ ┴ ┴
src └──────┘ ┴┴┴ ┴└─────┘┴ ┴┴┴┴└──────┘┴ ┴ └───┘ ┴└────┘ └─
typ └──────┘ ┴┴┴ ┴└─────┘┴ ┴┴┴┴└──────┘┴ ┴┴ └───┘ ┴└────┘┴└─
doc └──────┘ ┴ ┴ ┴└─────┘┴ ┴┴┴┴└──────┘┴ ┴ └───┘ ┴└────┘ └─
txt └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴└────┘ └─
par └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴└────┘ └─
pid └───┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └─────┘ └─
st ─────────────────────────────────────────────────────┘└─────────
328 ... = univ : dense_Union_interior_of_closed hc hU,
id └──┘ └────────────────────────────┘ └┘ └┘
src ────────────────┘└──┘ ┴└──┘└─┘└────────────────────────────┘┴ ┴
typ ────────────────┘└──┘ ┴└──┘└─┘└────────────────────────────┘┴└┘┴└┘
doc ────────────────┘└──┘ ┴ └─┘└────────────────────────────┘┴ ┴
txt ────────────────┘└──┘ ┴ └─┘ ┴ ┴
par ────────────────┘└──┘ ┴ └─┘ ┴ ┴
pid ────────────────────┘ ┴ └─┘ ┴ ┴
st ────────────────┘└───────────────────────────────────────────────┘└─
329 exact univ_nonempty.ne_empty this.symm },
id └────────────────────┘ └───────┘
src └────┘└────────────────────┘┴└───────┘┴
typ └────┘└────────────────────┘┴└───────┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ──────────────────────────────────────────┘└┘└
330 rcases this with ⟨s, hs⟩,
id └──┘
src └─────┘ └───────────┘
typ └─────┘└──┘└───────────┘
doc └─────┘ └───────────┘
txt └─────┘ └───────────┘
par └─────┘ └───────────┘
pid ┴ └───────────┘
st ─────────────────────────┘└─
331 rcases hs with ⟨x, hx⟩,
id └┘
src └─────┘ └───────────┘
typ └─────┘└┘└───────────┘
doc └─────┘ └───────────┘
txt └─────┘ └───────────┘
par └─────┘ └───────────┘
pid ┴ └───────────┘
st ───────────────────────┘└─
332 rcases mem_nhds_iff.1 (mem_interior_iff_mem_nhds.1 hx) with ⟨ε, εpos, hε⟩,
id └──────────┘ └───────────────────────┘ └┘
src └─────┘└──────────┘└─┘ └───────────────────────┘└─┘ └──────────────────┘
typ └─────┘└──────────┘└─┘ └───────────────────────┘└─┘└┘└──────────────────┘
doc └─────┘ └─┘ └─┘ └──────────────────┘
txt └─────┘ └─┘ └─┘ └──────────────────┘
par └─────┘ └─┘ └─┘ └──────────────────┘
pid ┴ └─┘ └─┘ └──────────────────┘
st ──────────────────────────────────────────────────────────────────────────┘└─
333 exact ⟨s, x, ε, εpos, hε⟩,
id ┴ ┴ ┴ └──┘ └┘
src └────┘ └┘ └┘ └┘ └┘ ┴
typ └────┘ ┴└┘┴└┘┴└┘└──┘└┘└┘┴
doc └────┘ └┘ └┘ └┘ └┘ ┴
txt └────┘ └┘ └┘ └┘ └┘ ┴
par └────┘ └┘ └┘ └┘ └┘ ┴
pid ┴ └┘ └┘ └┘ └┘ ┴
st ──────────────────────────┘└─
334 end
st ──┘
335
336 end Baire_theorem